Require Import Int.
Require Import List.
Require Import String.
Require Import Datatypes.

(** Definition of Fin and Vector **)
(** Fin **)
Inductive Fin : nat -> Set :=  
| finNil : forall n, Fin (S n)
| finSuc : forall n, Fin n -> Fin (S n).
Implicit Arguments finSuc [n].


Definition fin_eqb (n : nat) : Fin n -> Fin n -> bool.
intros.
induction H.
inversion H0.
apply true.
apply false.
inversion H0.
apply false.
apply IHFin.
apply H2.
Defined.
Implicit Arguments fin_eqb [n].


Eval compute in (fin_eqb (finNil 1) (finSuc (finNil 0))).
Eval compute in (fin_eqb (finNil 1) (finNil 1)).
Eval compute in (fin_eqb (finSuc (finNil 0))(finSuc (finNil 0))).
Eval compute in (fin_eqb (finSuc (finNil 0)) (finNil 1)).


(* 
  := fun i j => match i with
                  | finNil n => match j with 
                                  | finNil n => true
                                  | _ => false
                              end
                  | finSuc i' => match j with
                                   | finNil => false
                                   | finSuc j' => fin_eqb i' j'
                                 end
                end.
*)


Definition list_fin_suc (n : nat) : list (Fin n) -> list (Fin (S n)) := map (finSuc (n := n)).
Implicit Arguments list_fin_suc [n].

(** enumerates all elements of fin n, for an n **)
Fixpoint enum_fin (n: nat) : list (Fin n) :=
  match n with
    | O => nil
    | S n' => finNil n' :: list_fin_suc (enum_fin n')
  end.
Eval compute in enum_fin 3.


  


    







